CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[1]∨LENGTH[5];

ELAPSED-TIME =8016

NIL 1 2
1 ¬(cb(m,x)∧(mv(y,x,b)∧(i(y)∧(i(x)∧t(x)))));3 4
2 mv(m,c,b);AXIOM
3 ¬(cb(m,x)∧(t(x)∧u(x,b)));5 6
4 mv(z,y,x)∧(i(z)∧(i(y)∧i(x)))⊃u(y,x)∨cl(x,f);AXIOM
5 ¬(t(x)∧(u(x,b)∧o(m,x)));7 8
6 cb(x,y)⊃o(x,y);AXIOM
7 ¬cl(m,b);9 10
8 t(y)∧(u(y,b)∧o(x,y))⊃cl(x,b);AXIOM
9 ¬r(m,b);THM
10 cl(x,y)∧a(x)⊃r(x,y);AXIOM